MAYBE 86.28 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/Monad.hs
H-Termination of the given Haskell-Program with start terms could not be shown:



↳ HASKELL
  ↳ LR

mainModule Monad
  ((mapAndUnzipM :: Monad b => (d  ->  b (c,a))  ->  [d]  ->  b ([c],[a])) :: Monad b => (d  ->  b (c,a))  ->  [d]  ->  b ([c],[a]))

module Monad where
  import qualified Maybe
import qualified Prelude
  mapAndUnzipM :: Monad d => (c  ->  d (a,b))  ->  [c]  ->  d ([a],[b])
mapAndUnzipM f xs = sequence (map f xs) >>= return . unzip


module Maybe where
  import qualified Monad
import qualified Prelude


Lambda Reductions:
The following Lambda expression
\xs→return (x : xs)

is transformed to
sequence0 x xs = return (x : xs)

The following Lambda expression
\x→sequence cs >>= sequence0 x

is transformed to
sequence1 cs x = sequence cs >>= sequence0 x

The following Lambda expression
\(a,b)~(as,bs)→(a : as,b : bs)

is transformed to
unzip0 (a,b) ~(as,bs) = (a : as,b : bs)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IPR

mainModule Monad
  ((mapAndUnzipM :: Monad c => (a  ->  c (b,d))  ->  [a]  ->  c ([b],[d])) :: Monad c => (a  ->  c (b,d))  ->  [a]  ->  c ([b],[d]))

module Maybe where
  import qualified Monad
import qualified Prelude

module Monad where
  import qualified Maybe
import qualified Prelude
  mapAndUnzipM :: Monad d => (c  ->  d (b,a))  ->  [c]  ->  d ([b],[a])
mapAndUnzipM f xs = sequence (map f xs) >>= return . unzip



IrrPat Reductions:
The variables of the following irrefutable Pattern
~(as,bs)

are replaced by calls to these functions
unzip00 (as,bs) = as

unzip01 (as,bs) = bs



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IPR
        ↳ HASKELL
          ↳ BR

mainModule Monad
  ((mapAndUnzipM :: Monad b => (a  ->  b (c,d))  ->  [a]  ->  b ([c],[d])) :: Monad b => (a  ->  b (c,d))  ->  [a]  ->  b ([c],[d]))

module Monad where
  import qualified Maybe
import qualified Prelude
  mapAndUnzipM :: Monad a => (b  ->  a (c,d))  ->  [b]  ->  a ([c],[d])
mapAndUnzipM f xs = sequence (map f xs) >>= return . unzip


module Maybe where
  import qualified Monad
import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IPR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR

mainModule Monad
  ((mapAndUnzipM :: Monad b => (d  ->  b (a,c))  ->  [d]  ->  b ([a],[c])) :: Monad b => (d  ->  b (a,c))  ->  [d]  ->  b ([a],[c]))

module Maybe where
  import qualified Monad
import qualified Prelude

module Monad where
  import qualified Maybe
import qualified Prelude
  mapAndUnzipM :: Monad c => (a  ->  c (d,b))  ->  [a]  ->  c ([d],[b])
mapAndUnzipM f xs = sequence (map f xs) >>= return . unzip



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IPR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL

mainModule Monad
  (mapAndUnzipM :: Monad d => (a  ->  d (c,b))  ->  [a]  ->  d ([c],[b]))

module Monad where
  import qualified Maybe
import qualified Prelude
  mapAndUnzipM :: Monad b => (c  ->  b (a,d))  ->  [c]  ->  b ([a],[d])
mapAndUnzipM f xs = sequence (map f xs) >>= return . unzip


module Maybe where
  import qualified Monad
import qualified Prelude